<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
 "http://www.w3.org/TR/html4/loose.dtd">
<!--
  Uses "almost standards mode", standard except for some table cell sizing.
  -->
<html>
<head>
  <meta http-equiv="content-type" content="text/html; charset=UTF-8">
  <title>Prooftoys - introduction to proofs</title>
  <link id=styles type="text/css" rel="stylesheet" href="logic.css">

<style type="text/css">

/* The SELECT element for choosing a sample */
select.sampleSelector {
  /* Override typically small browser font choices here. */
  font-size: small;
  font: -webkit-control;
}

</style>
<script src="boilerplate.js"></script>
</head>

<body>

<h1>Introduction to Prooftoys Proofs</h1>

<div id=slogans>
<!-- slogans here -->
</div>

<span id=leftNav>
<!-- Boilerplate HTML goes here -->
</span>

<span id=content>

<p>
This page introduces you to the language used in the Prooftoys
system, viewing and exploring proofs, and using the interactive proof
builder.

<h2>The language</h2>
<p>
For more complete information see the
<a href="http://code.google.com/p/prooftoys/wiki/LanguageSummary">
language documentation</a> in the project Wiki.
<p>
Aside from variables and constants, the language has only function
calls and function expressions.  The parser and printer support infix
operators, which are represented internally as function calls.
<p>
<b>Infix operators.</b>
Infix operators available in order of increasing precedence are:
<ul>
<li><code>==</code> (equivalence, displays as "<s>==</s>")
<li><code>==></code> (implication, displays as "<s>==></s>")
<li><code>|</code> (or)
<li><code>&</code> (and)
<li><code>= != &lt; &lt;= &gt; &gt;=</code>
(equality and relational operators)<br>
These display as <s>= != &lt; &le; &gt; &ge;</s> respectively.
<li><code>+ -</code>
<li><code>* /</code>
</ul>
<p>
<b>Negation ("not").</b>
Negation is represented by <s>not</s>, and acts like any other
function.  So "x is not red" might be expressed in Prooftoys
as <s>not (red x)</s>.  Like the Prooftoys functions for "and", "or",
its input is a true/false value and so is the value of its result.
<p>
<b>Function calls.</b>
Ordinary function calls look like <s>(f x)</s> or
<s>f x</s>.  An expression such as <s>sin x / 2</s> has the same
meaning as <s>(sin x) / 2</s>, <b>not</b> <s>sin(x / 2)</s>.  We say
that function calls have higher precedence than infix operators, just
as multiplication has higher precedence than addition, so that
when some parentheses are omitted in an expression such as
<s>x + 2 * y</s>, it has the same meaning as <s>x + (2 * y)</s>.
<p>
<b>Forall and exists.</b>
These quantifiers are entered as <code>forall</code> and
<code>exists</code>, and display as the usual mathematical symbols
<span class=math>&forall;</span> and <span class=math>&exist;</span>.
In Prooftoys the typical math notation
<span class=math>&forall;<i>x</i> <i>P</i>(<i>x</i>)</span>
is entered as <code>forall {x. P x}</code> or
<code>forall {x. (P x)}</code> and displays as
<s>forall {x. P x}</s> or <s>forall {x. (P x)}</s>.

<p>
<b>Function expressions.</b>
These have the form <s>{x. P x}</s>.  In an example like this one,
assuming <s>P</s> returns a true/false value, the notation can be read
like the common notation for sets, "<i>the set of x such that P of
x</i>".  In fact the <s>P x</s> part can be any expression, and the
whole thing can always be read as "<i>the function of <s>x</s> whose
value is <s>P x</s></i>".
<p>
The most common use of function expressions is with the quantifiers
<code>forall</code> (<s>forall</s>) and <code>exists</code>
(<s>exists</s>) as in the examples above, although usually in these
cases our attention focuses on the quantifier itself and not on the
the function expression.

<h2>Inference in Prooftoys</h2>
<p>
Prooftoys supports the usual forms of classical inference and has a
number of common rules predefined (though not yet inference with
existential quantifiers).
<p>
Its one fundamental rule of inference is the Q<sub>0</sub> Rule R that
allows replacement of any occurrence of a term by a term that is equal
to it.  The Prooftoys <s>replace</s> rule is the same
as the Q<sub>0</sub> derived Rule R', which does the same sort of
replacement when the equation is conditional.  In other words it
allows <s>C</s> to be replaced by <s>D</s> if
<s>H ==> (C = D)</s>.
It turns out that most equations in basic textbook algebra problems
have this form when written out in full, which makes this rule
especially useful.  See the section
<a href="real-numbers.html">Working with Real Numbers</a>.

<a name=sample-proofs></a>
<h2>Viewing and exploring proofs</h2>
<p>
Examples of many of the currently-implemented rules of inference are
available here.  Selecting a theorem or inference rule below displays
an example of usage of the rule or theorem.  Axioms, theorems, and
rules of inference often have parameters.
<p>
Some often-used practical rules of inference are universal
generalization ("add forall"), universal instantiation ("instantiate
forall"), and reasoning by cases ("proof by cases").  There is also a
tautology checker which can prove arbitrary tautologies.
<p>
To see how a rule operates internally, click on its name in the proof
line that uses it.
<p>
Note: <i>Proof displays are supported in modern browsers such as
Chrome, Firefox, Safari, and Internet Explorer 9.</i>

<p style="margin: 1.5em 1.5em .5em">
<b>Select a rule or theorem to prove:</b><span id=selectHolder></span>

<div id=proofDisplay style="margin-bottom: 1em"></div>
<a href="javascript:void jQuery('#proof-display-video').toggleClass('hidden')">
 Demo screencast
</a>

<object id="proof-display-video"  width="919" height="464"
 class=hidden style="border: 2px solid silver"
 type="application/x-shockwave-flash"
 data="http://content.screencast.com/users/CrisPerdue/folders/Jing/media/6c5bfb10-921d-49fa-be64-9986cea01d08/jingswfplayer.swf" >
 <param name="movie" value="http://content.screencast.com/users/CrisPerdue/folders/Jing/media/6c5bfb10-921d-49fa-be64-9986cea01d08/jingswfplayer.swf" />
 <param name="quality" value="high" />
 <param name="bgcolor" value="#FFFFFF" />
 <param name="flashVars"
  value="thumb=http://content.screencast.com/users/CrisPerdue/folders/Jing/media/6c5bfb10-921d-49fa-be64-9986cea01d08/FirstFrame.jpg&containerwidth=919&containerheight=464&content=http://content.screencast.com/users/CrisPerdue/folders/Jing/media/6c5bfb10-921d-49fa-be64-9986cea01d08/00000011.swf&blurover=false" />
 <param name="allowFullScreen" value="true" />
 <param name="scale" value="showall" />
 <param name="allowScriptAccess" value="always" />
 <param name="base"
  value="http://content.screencast.com/users/CrisPerdue/folders/Jing/media/6c5bfb10-921d-49fa-be64-9986cea01d08/"
 />
 Unable to display content. Adobe Flash is required.
</object>

<p>
<b>Assumptions.</b>
Most math problems start with assumptions, and whethere the
assumptions are stated explicitly or not, the assumptions are often
required to properly justify many of the steps in a problem
solution.
<p>
The Prooftoys language has a compact notation for referring to
assumptions.  For example if an assumption is made in line 1 of a
proof, later steps can refer to that assumption using the number 1,
something like this:
<blockquote>
1. <s>x / 4 = y</s> (assumption)<br>
2. <s>1: x = 4 * y</s><br>
3. <s>y = 5</s> (assumption)<br>
4. <s>1, 3: x = 20</s>
</blockquote>
Here Line 2 refers to the assumption on line 1, and
line 4 refers to the assumptions on lines 1 and 3.
Line 2 is a shorthand for:
<blockquote>
2. <s>x / 4 = y ==> x = 4 * y</s>
</blockquote>
and line 4 similarly is just a shorthand for:
<blockquote>
4. <s>(x / 4 = y & y = 5) ==> x = 20</s>
</blockquote>

<h2>Using the proof builder</h2>
<p>
The proof builder lets you interactively build proofs using all of the
publicly-available theorems and rules of inference.  It can make
working with proofs easier, apply rules of inference correctly,
show what inference rules do and how they work.
<p>
To start, click on the text entry field.  It will pop up a menu of all
axioms, theorems, and theorem schemas available.  You can start typing
the name you want or select it from the list.  Clicking on the desired
item or typing <code>&lt;Enter&gt;</code> when it is selected will choose it.
<p>
Once you have chosen the axiom or theorem to use, the system checks
whether it takes parameters.  If so, you will be offered a small form
to fill in.  Enter expressions in the language as needed and type
<code>&lt;Enter&gt;</code> to submit the form.  The system will prove
the theorem as needed and display it in the proof.  A common first
step in solving a math problem is to use the <s>assume</s> theorem
schema.  Type any expression, and it will be "assumed" for you.  The
new theorem just says that your assumption implies itself, which is
obvious but works well with the rules of inference.
<p>
Once there is at least one step in your proof you can choose rules of
inference that take existing proof steps as input.  To use a rule of
inference, <i>select a step</i> that it depends on.  If a rule of
inference operates on a specific location in a step, you
must <i>select the subexpression</i> to operate on.  For example
rules <s>r</s> and <s>replace</s> require you to select
the subexpression you want to replace.  Click again on a step to
deselect it, to enter an axiom or theorem.

<h3>Building a simple proof</h3>
<p>
Let us consider a very simple example applying forward reasoning with
implications ("modus ponens") to a pair of assumptions.  Here is a
display of the proof you are going to build.
<p>
<div id=modusPonens></div>
<p>
In the Proof Builder area below, you can create the same proof.  To
enter an assumption click in the text entry field and select the rule
<s>assume hypothetically</s>.  Type in <code>p</code>, and press
<code>&lt;Enter&gt;</code>.  You will see the first line of your proof.
<p>
Next use the rule <s>assume hypothetically</s> again, typing in
<code>p ==> q</code> as your second assumption.
<p>
For the inference step, click on the step number "1" at the <i>very
beginning</i> in the first line of the proof display.  The whole line
will highlight itself (in yellow) and stay highlighted as you move the
mouse away.  Now use the dropdown list control to select a rule of
inference to use.  When you select <s>[p] and [p ==> q] to [q]</s> from the
list, a small form will appear with "1" as the hypothesis step.  Enter
<code>2</code> as the number of the implication step to apply the rule
to.  Press <code>&lt;Enter&gt;</code>.  You should see the conclusion
<s>q</s> added to the proof.
<p>
Note that in this rule <s>[p]</s>, <s>[p ==> q]</s>, and <s>[q]</s> are
patterns.  The rule needs two steps as its inputs, which must match
the patterns <s>[p]</s> and <s>[p ==> q]</s>.  <s>p</s> can be any
expression, but it must be the same in both of the input steps.  The
result of the inference will be the expression that matches with
<s>q</s> in the second input step.  The brackets just indicate the
boundaries of each of the patterns.
<p>
To make the assumptions explicit, you might wish to select the
last line of the proof and choose the <s>assumptions explicit</s>
rule, which causes the hypotheses to be displayed explicitly as
preconditions.  Again, select the entire step by clicking on the step
number.
<p>
Going beyond what is displayed in the sample, you could choose
<s>add forall</s> to add universal quantifiers to the formula.
Do this twice to quantify over both <s>p</s> and <s>q</s>.
<p>
<a href="javascript:void jQuery('#proofbuilder-video').toggleClass('hidden')">
 Proof Builder demo screencast
</a>
<p>
<!-- copy and paste. Modify height and width if desired. -->
<object id="proofbuilder-video"  width="932" height="228"
 class=hidden style="border: 2px solid silver"
 type="application/x-shockwave-flash"
 data="http://content.screencast.com/users/CrisPerdue/folders/Jing/media/3889e893-5603-4161-a04e-d669db2b86b3/jingswfplayer.swf"
 >
 <param name="movie"
 value="http://content.screencast.com/users/CrisPerdue/folders/Jing/media/3889e893-5603-4161-a04e-d669db2b86b3/jingswfplayer.swf"
 />
 <param name="quality" value="high" />
 <param name="bgcolor" value="#FFFFFF" />
 <param name="flashVars"
 value="thumb=http://content.screencast.com/users/CrisPerdue/folders/Jing/media/3889e893-5603-4161-a04e-d669db2b86b3/FirstFrame.jpg&containerwidth=932&containerheight=228&content=http://content.screencast.com/users/CrisPerdue/folders/Jing/media/3889e893-5603-4161-a04e-d669db2b86b3/00000006.swf&blurover=false"
 />
 <param name="allowFullScreen" value="true" />
 <param name="scale" value="showall" />
 <param name="allowScriptAccess" value="always" />
 <param name="base"
 value="http://content.screencast.com/users/CrisPerdue/folders/Jing/media/3889e893-5603-4161-a04e-d669db2b86b3/"
 />
 Unable to display content. Adobe Flash is required.
</object>
<p style="margin: 0em">
<b>Proof Builder</b>
<p>
<div id=proofEditor></div>

</span> <!-- content -->

<!-- Storage for state to preserve across page unloads -->
<textarea id=ToyStore rows=20 cols=80 class=hidden></textarea>
<!-- Force some white space to accommodate the autocompleter menu. -->
<div style="height: 20em"></div>

<!-- END OF HTML -->

<script src=sample-proofs.js></script>
<script>
// For emacs: '

// Insert boilerplate.
Toy.insertNav();
Toy.insertSlogans();
Toy.mathifyAll();

// On DOM ready:
jQuery(function() {
  // Set up some useful constants and functions.
  var rules = Toy.rules;

  // Modus ponens
  var mp1 = rules.assume('p');
  var mp2 = rules.assume('p ==> q');
  var mp3 = rules.forwardChain(mp1, mp2);
  var mp4 = rules.asImplication(mp3);
  Toy.renderProof(mp4, $('#modusPonens'));

  Toy.setUpSampleProofs('#selectHolder', '#proofDisplay', false);

  // Full proof editor
  var editor = new Toy.ProofEditor();
  window.proofEditor = editor;  // debugging
  editor.setEditable(true);
  $('#proofEditor').append(editor.containerNode);

});

</script>
</body>
</html>
